Reversible Programming

"Invertible programming languages specify transformations to be run in two directions. Partial invertibility lets invertible code be parameterized by the results of non-invertible code, whereas local invertibility requires all code to be invertible. The former allows for more flexible programming, while the latter has connections to domains such as low-energy computing and quantum computing.

In this paper, we identify four core constructs for partially invertible programming, and show how to give them a locally invertible interpretation. We show the expressiveness of the constructs by designing the functional invertible language Kalpis, and show how to give them a locally invertible semantics using the novel arrow combinator language rrArr."

Seminar

• Paper
  • Kalpis: an Arrow-based Locally and Partially Invertible System
• Tool
  • Git

Project

In a project, we will implementing a simple DSL following the strategy described above in the paper about reversible programming in Lean. Lean is a modern, general-purpose programming language featuring advanced functional programming constructs such as pattern matching, recursion, immutable datastructures, type classes, dependent types and more. At the same time, Lean compiles to C++, featuring easy interopability with low-level libraries where necessary. Let's try it out and see how far we can go :)